Type Bytes.fromList with an all-literal in-range list as total - #808

Bytes.fromList([0, 10, 255]) types as plain Bytes and constructs the value directly — no ?, no match. Any other argument shape keeps Result<Bytes, String> exactly as before: an identifier, a computed list, a computed element, an out-of-range literal ([65, 256]), a negative one, or a magnitude beyond i64. The empty list discharges vacuously.

The gate is derived, not named

Nothing in the rule mentions Bytes, fromList, or 0..=255. src/analysis/literal_refinement.rs builds the table from two recognizers that already existed:

• analysis::shape::detect_module_patterns supplies the RefinementSmartConstructor pattern (carrier field + validating predicate);
• the packed layout's element-interval derivation, factored out of packed_sequence.rs as element_interval_from_predicate, supplies the bound.

Sharing the second step is the load-bearing part. A packed carrier writes elements into a raw i8 array with no range check, so "the discharge admits this value" and "the packed layout can store it" must be one predicate — they now are, literally the same function. A user refinement with a different range discharges against that range; a record with no validating constructor never discharges.

The table lives on the SymbolTable: the single place entry items and dependency modules are jointly in hand, and the right coupling — a call that cannot resolve cannot discharge. The typechecker and the HIR resolver read that one table, which is what keeps the checked and unchecked pipelines from forking.

Two design points worth review

Spelling insensitivity is forced, not chosen. flatten_multimodule renames a dependency's fromList to a prefixed bare name and rewrites both the qualified and the in-module call sites to it before the wasm-gc backend re-resolves. After the flatten the two spellings are indistinguishable, so a qualified-only rule would discharge before it and not after. Consequence: stdlib/bytes.av's own verify fromList block migrates; a non-literal Ok case was added so the Result contract keeps its coverage. Two refinements sharing a bare constructor name are fail-closed.

The lowering is a construct site, not a call. RecordCreate is total on all four backends and needs no new IR node; proof_lower::multi_field_record_demotions already treats a construct site whose every value is a literal inside the proven interval as exactly as gated as the smart constructor. The rewrite runs on resolved HIR, so the AST-walking demotion scans still see only the constructor call. The alternative — a new UnwrapOk intrinsic — needs a VM opcode plus Rust and wasm-gc arms and has no workable Lean or Dafny story (Bytes has no Inhabited; ? is unsupported in Dafny).

Proof backends

Lean emits ⟨[0, 10, 255], by …⟩, so the kernel re-establishes the gate's own claim instead of assuming it. allInRange is compiled by well-founded recursion, which decide cannot evaluate through the elaborator, so the ladder gains a final simp [<predicate>] rung whose name is read off the refinement's invariant. Dafny discharges the same fact as a subset-type constraint. tests/fixtures/discharged_bytes_law.av is gated by both at budget 0; the 32-element stress case lives in a Lean-only fixture, because Dafny's default function fuel does not unfold a sequence that long.

Migration is loud

A Result / Option constructor pattern whose subject is neither is now a type error. Without it match Bytes.fromList([1, 2]) would silently walk off the end at runtime. Two diagnostic slugs with repair hints were added (error-prop-non-result, pattern-subject-mismatch).

Self-host

Refused, not silently diverged. The Aver-in-Aver resolver has no refinement recognizer — no type defs, no dependency ASTs, no interval derivation — so a mirror is not the three syntactic predicates the literal-divisor rule needed. aver run --self-host and the self-host replay backend now reject a discharged program with an error naming the call sites; the pre-gate symptom was a bare field access on non-record.

Tests

• Boundary pins named after the boundary, including every fallback shape (tests/typechecker_spec.rs).
• wasm-gc differential: a discharged literal keeps the proof-derived packed layout (type-section assertion: exactly one more i8 array than the boxed build) and agrees with the VM; the out-of-interval literal declines on all three legs (tests/wasm_gc_packed_sequence.rs).
• VM / wasm-gc / generated-Rust agreement with discharged and fallible calls in one program (tests/cross_backend_stress.rs, tests/rust_codegen_differential.rs).
• Lean + Dafny fixtures above; self-host rejection test.

Notes

• Coverage counter: 77 → 81, zero regressions. The +4 are projects/k5_fdiv functions that Type Int.div and Int.mod with a nonzero literal divisor as total #806's literal-divisor discharge made certifiable; they only surface now because thirteen workflow_engine units were failing to compile on an unmigrated Result.withDefault(Int.div(prev, 4), 0) left over from that PR. projects/workflow_engine/domain/time.av is migrated here so the corpus builds again. tools/coverage-baseline.json is left untouched — refreshing the headline is a separate call.
• src/analysis/ already depends on codegen::common and codegen::ModuleInfo, so the new module introduces no new layering direction.

🤖 Generated with Claude Code